(1
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 58)
  ("(var3 stable)" 58 281)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 59)
  ("(var4 stable)" 59 281)
  ("(var1 stable)" 0 31)
  ("(var1 up)" 31 59)
  ("(var1 stable)" 59 281)
  ("(var2 stable)" 0 46)
  ("(var2 up)" 46 48)
  ("(var2 down)" 48 51)
  ("(var2 up)" 51 219)
  ("(var2 stable)" 219 281)
 )
)
(2
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 118)
  ("(var3 stable)" 118 362)
  ("(var4 stable)" 0 91)
  ("(var4 up)" 91 124)
  ("(var4 stable)" 124 362)
  ("(var1 stable)" 0 92)
  ("(var1 up)" 92 120)
  ("(var1 stable)" 120 362)
  ("(var2 stable)" 0 107)
  ("(var2 up)" 107 109)
  ("(var2 down)" 109 114)
  ("(var2 up)" 114 247)
  ("(var2 stable)" 247 362)
 )
)
(3
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 41)
  ("(var3 down)" 41 43)
  ("(var3 up)" 43 69)
  ("(var3 stable)" 69 71)
  ("(var3 up)" 71 73)
  ("(var3 stable)" 73 300)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 65)
  ("(var4 stable)" 65 69)
  ("(var4 up)" 69 71)
  ("(var4 stable)" 71 300)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 70)
  ("(var1 stable)" 70 300)
  ("(var2 stable)" 0 53)
  ("(var2 up)" 53 55)
  ("(var2 down)" 55 60)
  ("(var2 stable)" 60 101)
  ("(var2 up)" 101 179)
  ("(var2 stable)" 179 298)
  ("(var2 down)" 298 300)
 )
)
(4
 (
  ("(var3 stable)" 0 86)
  ("(var3 up)" 86 94)
  ("(var3 down)" 94 96)
  ("(var3 up)" 96 133)
  ("(var3 stable)" 133 376)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 86)
  ("(var4 stable)" 86 90)
  ("(var4 up)" 90 121)
  ("(var4 stable)" 121 376)
  ("(var1 stable)" 0 87)
  ("(var1 up)" 87 125)
  ("(var1 stable)" 125 376)
  ("(var2 stable)" 0 107)
  ("(var2 up)" 107 112)
  ("(var2 down)" 112 116)
  ("(var2 stable)" 116 158)
  ("(var2 up)" 158 222)
  ("(var2 stable)" 222 224)
  ("(var2 up)" 224 244)
  ("(var2 down)" 244 247)
  ("(var2 stable)" 247 376)
 )
)
(5
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 102)
  ("(var3 stable)" 102 323)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 106)
  ("(var4 stable)" 106 323)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 108)
  ("(var1 down)" 108 110)
  ("(var1 stable)" 110 323)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 stable)" 96 141)
  ("(var2 up)" 141 220)
  ("(var2 stable)" 220 323)
 )
)
(6
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 104)
  ("(var3 stable)" 104 336)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 70)
  ("(var4 stable)" 70 72)
  ("(var4 up)" 72 103)
  ("(var4 down)" 103 105)
  ("(var4 up)" 105 107)
  ("(var4 stable)" 107 336)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 105)
  ("(var1 stable)" 105 336)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 95)
  ("(var2 stable)" 95 136)
  ("(var2 up)" 136 220)
  ("(var2 down)" 220 222)
  ("(var2 stable)" 222 336)
 )
)
(7
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 72)
  ("(var3 stable)" 72 312)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 74)
  ("(var4 stable)" 74 312)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 65)
  ("(var1 stable)" 65 67)
  ("(var1 up)" 67 73)
  ("(var1 stable)" 73 312)
  ("(var2 stable)" 0 56)
  ("(var2 up)" 56 60)
  ("(var2 down)" 60 63)
  ("(var2 up)" 63 213)
  ("(var2 stable)" 213 312)
 )
)
(8
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 121)
  ("(var3 stable)" 121 365)
  ("(var4 stable)" 0 81)
  ("(var4 up)" 81 118)
  ("(var4 stable)" 118 365)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 122)
  ("(var1 stable)" 122 365)
  ("(var2 stable)" 0 103)
  ("(var2 up)" 103 105)
  ("(var2 down)" 105 110)
  ("(var2 up)" 110 236)
  ("(var2 down)" 236 238)
  ("(var2 up)" 238 240)
  ("(var2 stable)" 240 363)
  ("(var2 down)" 363 365)
 )
)
(9
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 110)
  ("(var3 stable)" 110 328)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 108)
  ("(var4 stable)" 108 111)
  ("(var4 up)" 111 113)
  ("(var4 stable)" 113 328)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 108)
  ("(var1 stable)" 108 328)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 96)
  ("(var2 down)" 96 99)
  ("(var2 up)" 99 270)
  ("(var2 stable)" 270 328)
 )
)
(10
 (
  ("(var3 stable)" 0 71)
  ("(var3 down)" 71 74)
  ("(var3 up)" 74 78)
  ("(var3 stable)" 78 80)
  ("(var3 up)" 80 97)
  ("(var3 stable)" 97 99)
  ("(var3 up)" 99 101)
  ("(var3 stable)" 101 313)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 100)
  ("(var4 stable)" 100 313)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 95)
  ("(var1 stable)" 95 313)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 stable)" 92 129)
  ("(var2 up)" 129 217)
  ("(var2 stable)" 217 313)
 )
)
(11
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 37)
  ("(var3 stable)" 37 39)
  ("(var3 up)" 39 63)
  ("(var3 stable)" 63 290)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 41)
  ("(var4 down)" 41 43)
  ("(var4 up)" 43 68)
  ("(var4 stable)" 68 290)
  ("(var1 stable)" 0 35)
  ("(var1 down)" 35 37)
  ("(var1 up)" 37 40)
  ("(var1 stable)" 40 42)
  ("(var1 up)" 42 73)
  ("(var1 stable)" 73 290)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 61)
  ("(var2 stable)" 61 98)
  ("(var2 up)" 98 174)
  ("(var2 stable)" 174 290)
 )
)
(12
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 86)
  ("(var3 stable)" 86 314)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 88)
  ("(var4 stable)" 88 314)
  ("(var1 stable)" 0 57)
  ("(var1 up)" 57 86)
  ("(var1 stable)" 86 88)
  ("(var1 up)" 88 90)
  ("(var1 stable)" 90 314)
  ("(var2 stable)" 0 73)
  ("(var2 up)" 73 75)
  ("(var2 down)" 75 79)
  ("(var2 up)" 79 188)
  ("(var2 stable)" 188 314)
 )
)
(13
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 99)
  ("(var3 stable)" 99 315)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 73)
  ("(var4 stable)" 73 75)
  ("(var4 up)" 75 101)
  ("(var4 stable)" 101 315)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 74)
  ("(var1 up)" 74 101)
  ("(var1 stable)" 101 315)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 stable)" 92 132)
  ("(var2 up)" 132 210)
  ("(var2 stable)" 210 315)
 )
)
(14
 (
  ("(var3 stable)" 0 93)
  ("(var3 up)" 93 122)
  ("(var3 stable)" 122 347)
  ("(var4 stable)" 0 88)
  ("(var4 up)" 88 119)
  ("(var4 stable)" 119 347)
  ("(var1 stable)" 0 87)
  ("(var1 up)" 87 116)
  ("(var1 stable)" 116 347)
  ("(var2 stable)" 0 103)
  ("(var2 up)" 103 105)
  ("(var2 down)" 105 110)
  ("(var2 stable)" 110 151)
  ("(var2 up)" 151 211)
  ("(var2 down)" 211 213)
  ("(var2 up)" 213 216)
  ("(var2 stable)" 216 347)
 )
)
(15
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 88)
  ("(var3 stable)" 88 303)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 89)
  ("(var4 stable)" 89 303)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 89)
  ("(var1 stable)" 89 303)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 82)
  ("(var2 stable)" 82 121)
  ("(var2 up)" 121 198)
  ("(var2 stable)" 198 303)
 )
)
(16
 (
  ("(var3 stable)" 0 105)
  ("(var3 up)" 105 131)
  ("(var3 stable)" 131 382)
  ("(var4 stable)" 0 104)
  ("(var4 up)" 104 141)
  ("(var4 stable)" 141 382)
  ("(var1 stable)" 0 98)
  ("(var1 up)" 98 136)
  ("(var1 stable)" 136 382)
  ("(var2 stable)" 0 120)
  ("(var2 up)" 120 123)
  ("(var2 down)" 123 127)
  ("(var2 stable)" 127 174)
  ("(var2 up)" 174 244)
  ("(var2 stable)" 244 382)
 )
)
(17
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 42)
  ("(var3 down)" 42 44)
  ("(var3 up)" 44 47)
  ("(var3 stable)" 47 49)
  ("(var3 up)" 49 72)
  ("(var3 stable)" 72 311)
  ("(var4 stable)" 0 36)
  ("(var4 up)" 36 69)
  ("(var4 stable)" 69 311)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 42)
  ("(var1 stable)" 42 44)
  ("(var1 up)" 44 74)
  ("(var1 stable)" 74 311)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 64)
  ("(var2 up)" 64 190)
  ("(var2 stable)" 190 311)
 )
)
(18
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 66)
  ("(var3 stable)" 66 306)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 73)
  ("(var4 stable)" 73 306)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 41)
  ("(var1 down)" 41 43)
  ("(var1 up)" 43 74)
  ("(var1 stable)" 74 306)
  ("(var2 stable)" 0 55)
  ("(var2 up)" 55 57)
  ("(var2 down)" 57 62)
  ("(var2 up)" 62 188)
  ("(var2 stable)" 188 306)
 )
)
(19
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 79)
  ("(var3 stable)" 79 311)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 71)
  ("(var4 stable)" 71 311)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 78)
  ("(var1 stable)" 78 311)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 58)
  ("(var2 down)" 58 62)
  ("(var2 stable)" 62 102)
  ("(var2 up)" 102 186)
  ("(var2 down)" 186 188)
  ("(var2 stable)" 188 311)
 )
)
(20
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 123)
  ("(var3 stable)" 123 369)
  ("(var4 stable)" 0 96)
  ("(var4 up)" 96 123)
  ("(var4 stable)" 123 369)
  ("(var1 stable)" 0 93)
  ("(var1 up)" 93 125)
  ("(var1 stable)" 125 127)
  ("(var1 up)" 127 129)
  ("(var1 stable)" 129 369)
  ("(var2 stable)" 0 109)
  ("(var2 up)" 109 111)
  ("(var2 down)" 111 116)
  ("(var2 stable)" 116 156)
  ("(var2 up)" 156 246)
  ("(var2 stable)" 246 369)
 )
)
(21
 (
  ("(var3 stable)" 0 79)
  ("(var3 up)" 79 118)
  ("(var3 stable)" 118 357)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 87)
  ("(var4 up)" 87 119)
  ("(var4 stable)" 119 357)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 116)
  ("(var1 stable)" 116 357)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 104)
  ("(var2 down)" 104 108)
  ("(var2 stable)" 108 147)
  ("(var2 up)" 147 229)
  ("(var2 stable)" 229 235)
  ("(var2 up)" 235 237)
  ("(var2 stable)" 237 357)
 )
)
(22
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 105)
  ("(var3 stable)" 105 346)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 107)
  ("(var4 stable)" 107 346)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 74)
  ("(var1 stable)" 74 77)
  ("(var1 up)" 77 79)
  ("(var1 stable)" 79 81)
  ("(var1 up)" 81 105)
  ("(var1 stable)" 105 346)
  ("(var2 stable)" 0 90)
  ("(var2 up)" 90 92)
  ("(var2 down)" 92 97)
  ("(var2 stable)" 97 143)
  ("(var2 up)" 143 222)
  ("(var2 stable)" 222 226)
  ("(var2 up)" 226 228)
  ("(var2 stable)" 228 346)
 )
)
(23
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 94)
  ("(var3 stable)" 94 342)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 90)
  ("(var4 stable)" 90 342)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 101)
  ("(var1 stable)" 101 342)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 85)
  ("(var2 up)" 85 207)
  ("(var2 stable)" 207 342)
 )
)
(24
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 67)
  ("(var3 stable)" 67 315)
  ("(var4 stable)" 0 27)
  ("(var4 up)" 27 63)
  ("(var4 stable)" 63 66)
  ("(var4 up)" 66 68)
  ("(var4 stable)" 68 315)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 67)
  ("(var1 stable)" 67 315)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 55)
  ("(var2 down)" 55 59)
  ("(var2 stable)" 59 105)
  ("(var2 up)" 105 161)
  ("(var2 down)" 161 163)
  ("(var2 up)" 163 205)
  ("(var2 stable)" 205 315)
 )
)
(25
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 84)
  ("(var3 stable)" 84 332)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 59)
  ("(var4 stable)" 59 61)
  ("(var4 up)" 61 88)
  ("(var4 stable)" 88 332)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 88)
  ("(var1 stable)" 88 332)
  ("(var2 stable)" 0 71)
  ("(var2 up)" 71 73)
  ("(var2 down)" 73 78)
  ("(var2 stable)" 78 121)
  ("(var2 up)" 121 217)
  ("(var2 stable)" 217 332)
 )
)
(26
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 104)
  ("(var3 stable)" 104 333)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 108)
  ("(var4 stable)" 108 333)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 108)
  ("(var1 stable)" 108 333)
  ("(var2 stable)" 0 87)
  ("(var2 up)" 87 89)
  ("(var2 down)" 89 94)
  ("(var2 up)" 94 211)
  ("(var2 stable)" 211 333)
 )
)
(27
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 95)
  ("(var3 stable)" 95 335)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 94)
  ("(var4 stable)" 94 335)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 97)
  ("(var1 stable)" 97 335)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 82)
  ("(var2 down)" 82 86)
  ("(var2 up)" 86 220)
  ("(var2 stable)" 220 335)
 )
)
(28
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 71)
  ("(var3 stable)" 71 281)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 71)
  ("(var4 stable)" 71 281)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 76)
  ("(var1 stable)" 76 281)
  ("(var2 stable)" 0 58)
  ("(var2 up)" 58 62)
  ("(var2 down)" 62 64)
  ("(var2 up)" 64 161)
  ("(var2 stable)" 161 281)
 )
)
(29
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 101)
  ("(var3 stable)" 101 317)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 100)
  ("(var4 stable)" 100 317)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 108)
  ("(var1 stable)" 108 317)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 stable)" 92 126)
  ("(var2 up)" 126 215)
  ("(var2 stable)" 215 317)
 )
)
(30
 (
  ("(var3 stable)" 0 93)
  ("(var3 up)" 93 118)
  ("(var3 stable)" 118 355)
  ("(var4 stable)" 0 94)
  ("(var4 up)" 94 118)
  ("(var4 stable)" 118 355)
  ("(var1 stable)" 0 93)
  ("(var1 up)" 93 122)
  ("(var1 stable)" 122 355)
  ("(var2 stable)" 0 105)
  ("(var2 up)" 105 107)
  ("(var2 down)" 107 112)
  ("(var2 up)" 112 216)
  ("(var2 stable)" 216 355)
 )
)
(31
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 111)
  ("(var3 stable)" 111 323)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 112)
  ("(var4 stable)" 112 323)
  ("(var1 stable)" 0 75)
  ("(var1 up)" 75 111)
  ("(var1 stable)" 111 323)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 96)
  ("(var2 down)" 96 101)
  ("(var2 up)" 101 207)
  ("(var2 down)" 207 209)
  ("(var2 up)" 209 211)
  ("(var2 stable)" 211 323)
 )
)
(32
 (
  ("(var3 stable)" 0 52)
  ("(var3 up)" 52 85)
  ("(var3 stable)" 85 330)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 79)
  ("(var4 down)" 79 81)
  ("(var4 stable)" 81 330)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 54)
  ("(var1 stable)" 54 56)
  ("(var1 up)" 56 81)
  ("(var1 stable)" 81 330)
  ("(var2 stable)" 0 65)
  ("(var2 up)" 65 67)
  ("(var2 down)" 67 72)
  ("(var2 stable)" 72 121)
  ("(var2 up)" 121 188)
  ("(var2 stable)" 188 219)
  ("(var2 down)" 219 221)
  ("(var2 up)" 221 223)
  ("(var2 stable)" 223 330)
 )
)
(33
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 88)
  ("(var3 stable)" 88 323)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 89)
  ("(var4 down)" 89 91)
  ("(var4 stable)" 91 323)
  ("(var1 stable)" 0 5)
  ("(var1 down)" 5 7)
  ("(var1 stable)" 7 60)
  ("(var1 up)" 60 89)
  ("(var1 stable)" 89 323)
  ("(var2 stable)" 0 71)
  ("(var2 up)" 71 75)
  ("(var2 down)" 75 80)
  ("(var2 stable)" 80 123)
  ("(var2 up)" 123 201)
  ("(var2 down)" 201 203)
  ("(var2 stable)" 203 323)
 )
)
(34
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 103)
  ("(var3 stable)" 103 336)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 107)
  ("(var4 stable)" 107 336)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 105)
  ("(var1 stable)" 105 336)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 up)" 96 233)
  ("(var2 stable)" 233 336)
 )
)
(35
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 71)
  ("(var3 stable)" 71 308)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 72)
  ("(var4 stable)" 72 308)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 76)
  ("(var1 stable)" 76 308)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 64)
  ("(var2 up)" 64 204)
  ("(var2 stable)" 204 308)
 )
)
(36
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 86)
  ("(var3 down)" 86 88)
  ("(var3 up)" 88 90)
  ("(var3 stable)" 90 328)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 50)
  ("(var4 down)" 50 53)
  ("(var4 up)" 53 85)
  ("(var4 stable)" 85 328)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 89)
  ("(var1 stable)" 89 328)
  ("(var2 stable)" 0 68)
  ("(var2 up)" 68 71)
  ("(var2 down)" 71 75)
  ("(var2 up)" 75 229)
  ("(var2 stable)" 229 328)
 )
)
(37
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 103)
  ("(var3 stable)" 103 362)
  ("(var4 stable)" 0 65)
  ("(var4 up)" 65 67)
  ("(var4 stable)" 67 70)
  ("(var4 up)" 70 107)
  ("(var4 stable)" 107 362)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 106)
  ("(var1 down)" 106 108)
  ("(var1 stable)" 108 362)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 88)
  ("(var2 down)" 88 93)
  ("(var2 up)" 93 232)
  ("(var2 stable)" 232 247)
  ("(var2 up)" 247 249)
  ("(var2 stable)" 249 362)
 )
)
(38
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 114)
  ("(var3 down)" 114 116)
  ("(var3 up)" 116 121)
  ("(var3 stable)" 121 364)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 120)
  ("(var4 stable)" 120 364)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 74)
  ("(var1 stable)" 74 80)
  ("(var1 up)" 80 82)
  ("(var1 stable)" 82 84)
  ("(var1 up)" 84 116)
  ("(var1 stable)" 116 364)
  ("(var2 down)" 0 2)
  ("(var2 stable)" 2 97)
  ("(var2 up)" 97 99)
  ("(var2 down)" 99 106)
  ("(var2 up)" 106 205)
  ("(var2 stable)" 205 207)
  ("(var2 up)" 207 249)
  ("(var2 stable)" 249 364)
 )
)
(39
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 89)
  ("(var3 stable)" 89 335)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 89)
  ("(var4 stable)" 89 335)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 63)
  ("(var1 stable)" 63 65)
  ("(var1 up)" 65 91)
  ("(var1 stable)" 91 335)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 83)
  ("(var2 stable)" 83 125)
  ("(var2 up)" 125 217)
  ("(var2 stable)" 217 335)
 )
)
(40
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 119)
  ("(var3 stable)" 119 359)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 117)
  ("(var4 stable)" 117 359)
  ("(var1 stable)" 0 87)
  ("(var1 up)" 87 114)
  ("(var1 stable)" 114 359)
  ("(var2 stable)" 0 102)
  ("(var2 up)" 102 104)
  ("(var2 down)" 104 109)
  ("(var2 up)" 109 246)
  ("(var2 stable)" 246 359)
 )
)
(41
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 79)
  ("(var3 stable)" 79 328)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 77)
  ("(var4 stable)" 77 328)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 79)
  ("(var1 stable)" 79 328)
  ("(var2 stable)" 0 60)
  ("(var2 up)" 60 64)
  ("(var2 down)" 64 68)
  ("(var2 stable)" 68 111)
  ("(var2 up)" 111 214)
  ("(var2 stable)" 214 328)
 )
)
(42
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 111)
  ("(var3 stable)" 111 355)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 107)
  ("(var4 stable)" 107 109)
  ("(var4 up)" 109 114)
  ("(var4 stable)" 114 355)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 81)
  ("(var1 stable)" 81 83)
  ("(var1 up)" 83 115)
  ("(var1 stable)" 115 355)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 100)
  ("(var2 down)" 100 105)
  ("(var2 up)" 105 227)
  ("(var2 stable)" 227 355)
 )
)
(43
 (
  ("(var3 stable)" 0 28)
  ("(var3 up)" 28 68)
  ("(var3 stable)" 68 291)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 64)
  ("(var4 stable)" 64 291)
  ("(var1 stable)" 0 31)
  ("(var1 up)" 31 35)
  ("(var1 stable)" 35 37)
  ("(var1 up)" 37 69)
  ("(var1 stable)" 69 291)
  ("(var2 stable)" 0 49)
  ("(var2 up)" 49 53)
  ("(var2 down)" 53 57)
  ("(var2 up)" 57 142)
  ("(var2 down)" 142 144)
  ("(var2 up)" 144 190)
  ("(var2 stable)" 190 291)
 )
)
(44
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 131)
  ("(var3 stable)" 131 372)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 82)
  ("(var4 stable)" 82 86)
  ("(var4 up)" 86 121)
  ("(var4 down)" 121 123)
  ("(var4 stable)" 123 372)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 123)
  ("(var1 stable)" 123 372)
  ("(var2 stable)" 0 99)
  ("(var2 up)" 99 105)
  ("(var2 down)" 105 109)
  ("(var2 up)" 109 241)
  ("(var2 stable)" 241 372)
 )
)
(45
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 76)
  ("(var3 stable)" 76 299)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 67)
  ("(var4 stable)" 67 299)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 65)
  ("(var1 stable)" 65 299)
  ("(var2 stable)" 0 53)
  ("(var2 up)" 53 55)
  ("(var2 down)" 55 60)
  ("(var2 up)" 60 170)
  ("(var2 stable)" 170 299)
 )
)
(46
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 82)
  ("(var3 stable)" 82 290)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 78)
  ("(var4 stable)" 78 290)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 75)
  ("(var1 stable)" 75 290)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 66)
  ("(var2 down)" 66 71)
  ("(var2 up)" 71 187)
  ("(var2 stable)" 187 290)
 )
)
(47
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 75)
  ("(var3 stable)" 75 77)
  ("(var3 up)" 77 103)
  ("(var3 stable)" 103 355)
  ("(var4 stable)" 0 66)
  ("(var4 up)" 66 109)
  ("(var4 stable)" 109 355)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 105)
  ("(var1 stable)" 105 355)
  ("(var2 stable)" 0 90)
  ("(var2 up)" 90 93)
  ("(var2 down)" 93 97)
  ("(var2 up)" 97 229)
  ("(var2 stable)" 229 355)
 )
)
(48
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 80)
  ("(var3 stable)" 80 83)
  ("(var3 up)" 83 107)
  ("(var3 stable)" 107 365)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 111)
  ("(var4 stable)" 111 365)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 78)
  ("(var1 stable)" 78 82)
  ("(var1 up)" 82 116)
  ("(var1 stable)" 116 365)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 98)
  ("(var2 down)" 98 103)
  ("(var2 stable)" 103 147)
  ("(var2 up)" 147 237)
  ("(var2 stable)" 237 365)
 )
)
(49
 (
  ("(var3 stable)" 0 86)
  ("(var3 up)" 86 129)
  ("(var3 stable)" 129 378)
  ("(var4 stable)" 0 93)
  ("(var4 up)" 93 123)
  ("(var4 stable)" 123 378)
  ("(var1 stable)" 0 87)
  ("(var1 up)" 87 89)
  ("(var1 stable)" 89 92)
  ("(var1 up)" 92 122)
  ("(var1 stable)" 122 378)
  ("(var2 stable)" 0 107)
  ("(var2 up)" 107 109)
  ("(var2 down)" 109 114)
  ("(var2 stable)" 114 157)
  ("(var2 up)" 157 226)
  ("(var2 down)" 226 228)
  ("(var2 up)" 228 230)
  ("(var2 stable)" 230 378)
 )
)
(50
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 83)
  ("(var3 stable)" 83 85)
  ("(var3 up)" 85 87)
  ("(var3 stable)" 87 301)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 83)
  ("(var4 stable)" 83 301)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 86)
  ("(var1 stable)" 86 301)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 up)" 79 195)
  ("(var2 stable)" 195 301)
 )
)
(51
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 79)
  ("(var3 stable)" 79 309)
  ("(var4 stable)" 0 54)
  ("(var4 up)" 54 79)
  ("(var4 stable)" 79 309)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 84)
  ("(var1 stable)" 84 309)
  ("(var2 stable)" 0 68)
  ("(var2 up)" 68 70)
  ("(var2 down)" 70 81)
  ("(var2 up)" 81 206)
  ("(var2 down)" 206 208)
  ("(var2 stable)" 208 309)
 )
)
(52
 (
  ("(var3 stable)" 0 48)
  ("(var3 down)" 48 50)
  ("(var3 up)" 50 76)
  ("(var3 stable)" 76 290)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 76)
  ("(var4 stable)" 76 290)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 74)
  ("(var1 stable)" 74 290)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 64)
  ("(var2 down)" 64 68)
  ("(var2 up)" 68 166)
  ("(var2 stable)" 166 290)
 )
)
(53
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 66)
  ("(var3 stable)" 66 283)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 64)
  ("(var4 stable)" 64 283)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 66)
  ("(var1 down)" 66 69)
  ("(var1 stable)" 69 283)
  ("(var2 stable)" 0 48)
  ("(var2 up)" 48 50)
  ("(var2 down)" 50 55)
  ("(var2 up)" 55 174)
  ("(var2 stable)" 174 283)
 )
)
(54
 (
  ("(var3 up)" 0 4)
  ("(var3 down)" 4 6)
  ("(var3 stable)" 6 82)
  ("(var3 up)" 82 111)
  ("(var3 stable)" 111 356)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 109)
  ("(var4 stable)" 109 356)
  ("(var1 stable)" 0 82)
  ("(var1 up)" 82 113)
  ("(var1 stable)" 113 356)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 98)
  ("(var2 down)" 98 103)
  ("(var2 stable)" 103 147)
  ("(var2 up)" 147 213)
  ("(var2 stable)" 213 356)
 )
)
(55
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 105)
  ("(var3 stable)" 105 354)
  ("(var3 down)" 354 356)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 104)
  ("(var4 down)" 104 106)
  ("(var4 stable)" 106 356)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 66)
  ("(var1 down)" 66 68)
  ("(var1 up)" 68 81)
  ("(var1 stable)" 81 83)
  ("(var1 up)" 83 110)
  ("(var1 stable)" 110 356)
  ("(var2 stable)" 0 87)
  ("(var2 up)" 87 89)
  ("(var2 down)" 89 94)
  ("(var2 up)" 94 230)
  ("(var2 stable)" 230 356)
 )
)
(56
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 65)
  ("(var3 stable)" 65 67)
  ("(var3 up)" 67 98)
  ("(var3 stable)" 98 333)
  ("(var4 stable)" 0 65)
  ("(var4 up)" 65 94)
  ("(var4 stable)" 94 333)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 99)
  ("(var1 stable)" 99 333)
  ("(var2 stable)" 0 81)
  ("(var2 up)" 81 83)
  ("(var2 down)" 83 88)
  ("(var2 up)" 88 188)
  ("(var2 stable)" 188 190)
  ("(var2 up)" 190 223)
  ("(var2 stable)" 223 333)
 )
)
(57
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 67)
  ("(var3 down)" 67 69)
  ("(var3 up)" 69 95)
  ("(var3 stable)" 95 344)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 98)
  ("(var4 stable)" 98 344)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 68)
  ("(var1 up)" 68 99)
  ("(var1 stable)" 99 101)
  ("(var1 up)" 101 103)
  ("(var1 stable)" 103 344)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 85)
  ("(var2 down)" 85 90)
  ("(var2 up)" 90 192)
  ("(var2 down)" 192 194)
  ("(var2 up)" 194 228)
  ("(var2 stable)" 228 344)
 )
)
(58
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 100)
  ("(var3 stable)" 100 333)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 99)
  ("(var4 down)" 99 101)
  ("(var4 stable)" 101 333)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 100)
  ("(var1 stable)" 100 333)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 up)" 92 210)
  ("(var2 stable)" 210 333)
 )
)
(59
 (
  ("(var3 stable)" 0 79)
  ("(var3 up)" 79 81)
  ("(var3 down)" 81 84)
  ("(var3 up)" 84 110)
  ("(var3 stable)" 110 361)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 109)
  ("(var4 stable)" 109 361)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 81)
  ("(var1 down)" 81 83)
  ("(var1 up)" 83 111)
  ("(var1 stable)" 111 361)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 98)
  ("(var2 down)" 98 103)
  ("(var2 up)" 103 245)
  ("(var2 stable)" 245 361)
 )
)
(60
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 66)
  ("(var3 stable)" 66 70)
  ("(var3 up)" 70 72)
  ("(var3 stable)" 72 321)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 68)
  ("(var4 down)" 68 70)
  ("(var4 stable)" 70 321)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 66)
  ("(var1 stable)" 66 321)
  ("(var2 stable)" 0 52)
  ("(var2 up)" 52 56)
  ("(var2 down)" 56 60)
  ("(var2 stable)" 60 103)
  ("(var2 up)" 103 194)
  ("(var2 down)" 194 196)
  ("(var2 stable)" 196 321)
 )
)
(61
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 58)
  ("(var3 up)" 58 90)
  ("(var3 stable)" 90 326)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 86)
  ("(var4 stable)" 86 326)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 93)
  ("(var1 stable)" 93 326)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 up)" 84 210)
  ("(var2 down)" 210 212)
  ("(var2 stable)" 212 326)
 )
)
(62
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 96)
  ("(var3 stable)" 96 316)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 90)
  ("(var4 stable)" 90 316)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 97)
  ("(var1 down)" 97 99)
  ("(var1 stable)" 99 316)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 86)
  ("(var2 up)" 86 207)
  ("(var2 down)" 207 209)
  ("(var2 stable)" 209 316)
 )
)
(63
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 68)
  ("(var3 stable)" 68 296)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 62)
  ("(var4 stable)" 62 296)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 40)
  ("(var1 up)" 40 68)
  ("(var1 stable)" 68 296)
  ("(var2 stable)" 0 53)
  ("(var2 up)" 53 55)
  ("(var2 down)" 55 58)
  ("(var2 up)" 58 226)
  ("(var2 stable)" 226 296)
 )
)
(64
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 111)
  ("(var3 stable)" 111 353)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 106)
  ("(var4 stable)" 106 108)
  ("(var4 up)" 108 110)
  ("(var4 down)" 110 112)
  ("(var4 stable)" 112 353)
  ("(var1 stable)" 0 75)
  ("(var1 up)" 75 108)
  ("(var1 stable)" 108 353)
  ("(var2 stable)" 0 91)
  ("(var2 up)" 91 93)
  ("(var2 down)" 93 98)
  ("(var2 up)" 98 197)
  ("(var2 down)" 197 199)
  ("(var2 up)" 199 229)
  ("(var2 stable)" 229 353)
 )
)
(65
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 59)
  ("(var3 stable)" 59 61)
  ("(var3 up)" 61 63)
  ("(var3 stable)" 63 292)
  ("(var4 stable)" 0 30)
  ("(var4 up)" 30 64)
  ("(var4 stable)" 64 292)
  ("(var1 stable)" 0 32)
  ("(var1 up)" 32 63)
  ("(var1 stable)" 63 292)
  ("(var2 stable)" 0 47)
  ("(var2 up)" 47 49)
  ("(var2 down)" 49 54)
  ("(var2 up)" 54 151)
  ("(var2 stable)" 151 154)
  ("(var2 up)" 154 186)
  ("(var2 stable)" 186 292)
 )
)
(66
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 103)
  ("(var3 stable)" 103 335)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 102)
  ("(var4 stable)" 102 335)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 103)
  ("(var1 stable)" 103 335)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 87)
  ("(var2 down)" 87 92)
  ("(var2 up)" 92 213)
  ("(var2 stable)" 213 335)
 )
)
(67
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 66)
  ("(var3 stable)" 66 295)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 67)
  ("(var4 stable)" 67 295)
  ("(var1 stable)" 0 29)
  ("(var1 up)" 29 70)
  ("(var1 stable)" 70 295)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 52)
  ("(var2 down)" 52 57)
  ("(var2 up)" 57 153)
  ("(var2 down)" 153 155)
  ("(var2 up)" 155 182)
  ("(var2 stable)" 182 295)
 )
)
(68
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 81)
  ("(var3 stable)" 81 294)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 82)
  ("(var4 stable)" 82 294)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 77)
  ("(var1 stable)" 77 294)
  ("(var2 stable)" 0 63)
  ("(var2 up)" 63 65)
  ("(var2 down)" 65 70)
  ("(var2 up)" 70 182)
  ("(var2 down)" 182 184)
  ("(var2 up)" 184 186)
  ("(var2 stable)" 186 290)
  ("(var2 down)" 290 292)
  ("(var2 up)" 292 294)
 )
)
(69
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 117)
  ("(var3 down)" 117 119)
  ("(var3 stable)" 119 361)
  ("(var4 stable)" 0 81)
  ("(var4 up)" 81 111)
  ("(var4 stable)" 111 361)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 113)
  ("(var1 stable)" 113 118)
  ("(var1 up)" 118 120)
  ("(var1 stable)" 120 361)
  ("(var2 stable)" 0 95)
  ("(var2 up)" 95 99)
  ("(var2 down)" 99 102)
  ("(var2 up)" 102 259)
  ("(var2 stable)" 259 361)
 )
)
(70
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 105)
  ("(var3 stable)" 105 332)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 104)
  ("(var4 stable)" 104 332)
  ("(var1 stable)" 0 78)
  ("(var1 up)" 78 107)
  ("(var1 stable)" 107 332)
  ("(var2 stable)" 0 92)
  ("(var2 up)" 92 94)
  ("(var2 down)" 94 99)
  ("(var2 up)" 99 216)
  ("(var2 down)" 216 218)
  ("(var2 up)" 218 222)
  ("(var2 stable)" 222 332)
 )
)
(71
 (
  ("(var3 up)" 0 2)
  ("(var3 stable)" 2 76)
  ("(var3 up)" 76 82)
  ("(var3 stable)" 82 84)
  ("(var3 up)" 84 109)
  ("(var3 stable)" 109 345)
  ("(var4 stable)" 0 82)
  ("(var4 up)" 82 108)
  ("(var4 stable)" 108 345)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 112)
  ("(var1 stable)" 112 345)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 96)
  ("(var2 down)" 96 101)
  ("(var2 up)" 101 225)
  ("(var2 stable)" 225 345)
 )
)
(72
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 56)
  ("(var3 up)" 56 82)
  ("(var3 stable)" 82 301)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 74)
  ("(var4 stable)" 74 76)
  ("(var4 up)" 76 81)
  ("(var4 stable)" 81 301)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 82)
  ("(var1 stable)" 82 301)
  ("(var2 stable)" 0 65)
  ("(var2 down)" 65 69)
  ("(var2 stable)" 69 108)
  ("(var2 up)" 108 196)
  ("(var2 stable)" 196 301)
 )
)
(73
 (
  ("(var3 stable)" 0 66)
  ("(var3 up)" 66 91)
  ("(var3 stable)" 91 307)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 98)
  ("(var4 stable)" 98 307)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 92)
  ("(var1 stable)" 92 307)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 stable)" 84 124)
  ("(var2 up)" 124 208)
  ("(var2 stable)" 208 307)
 )
)
(74
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 117)
  ("(var3 stable)" 117 354)
  ("(var4 stable)" 0 87)
  ("(var4 down)" 87 89)
  ("(var4 up)" 89 110)
  ("(var4 stable)" 110 112)
  ("(var4 up)" 112 115)
  ("(var4 stable)" 115 354)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 110)
  ("(var1 stable)" 110 112)
  ("(var1 up)" 112 121)
  ("(var1 stable)" 121 354)
  ("(var2 stable)" 0 102)
  ("(var2 up)" 102 104)
  ("(var2 down)" 104 109)
  ("(var2 stable)" 109 152)
  ("(var2 up)" 152 247)
  ("(var2 stable)" 247 354)
 )
)
(75
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 99)
  ("(var3 stable)" 99 354)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 95)
  ("(var4 stable)" 95 354)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 102)
  ("(var1 stable)" 102 354)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 85)
  ("(var2 down)" 85 89)
  ("(var2 stable)" 89 130)
  ("(var2 up)" 130 227)
  ("(var2 down)" 227 229)
  ("(var2 stable)" 229 354)
 )
)
(76
 (
  ("(var3 stable)" 0 87)
  ("(var3 up)" 87 118)
  ("(var3 down)" 118 120)
  ("(var3 stable)" 120 356)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 112)
  ("(var4 stable)" 112 114)
  ("(var4 up)" 114 121)
  ("(var4 stable)" 121 356)
  ("(var1 stable)" 0 83)
  ("(var1 up)" 83 117)
  ("(var1 stable)" 117 356)
  ("(var2 stable)" 0 101)
  ("(var2 up)" 101 103)
  ("(var2 down)" 103 108)
  ("(var2 stable)" 108 150)
  ("(var2 up)" 150 230)
  ("(var2 stable)" 230 356)
 )
)
(77
 (
  ("(var3 stable)" 0 65)
  ("(var3 up)" 65 99)
  ("(var3 stable)" 99 334)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 106)
  ("(var4 stable)" 106 334)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 100)
  ("(var1 stable)" 100 334)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 85)
  ("(var2 down)" 85 90)
  ("(var2 up)" 90 209)
  ("(var2 stable)" 209 334)
 )
)
(78
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 90)
  ("(var3 stable)" 90 308)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 63)
  ("(var4 up)" 63 89)
  ("(var4 stable)" 89 308)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 91)
  ("(var1 stable)" 91 308)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 83)
  ("(var2 stable)" 83 120)
  ("(var2 up)" 120 200)
  ("(var2 stable)" 200 308)
 )
)
(79
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 68)
  ("(var3 stable)" 68 293)
  ("(var4 up)" 0 2)
  ("(var4 down)" 2 4)
  ("(var4 stable)" 4 43)
  ("(var4 up)" 43 72)
  ("(var4 stable)" 72 293)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 69)
  ("(var1 stable)" 69 293)
  ("(var2 stable)" 0 55)
  ("(var2 up)" 55 57)
  ("(var2 down)" 57 62)
  ("(var2 up)" 62 148)
  ("(var2 stable)" 148 150)
  ("(var2 up)" 150 176)
  ("(var2 stable)" 176 293)
 )
)
(80
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 39)
  ("(var3 stable)" 39 41)
  ("(var3 up)" 41 72)
  ("(var3 down)" 72 74)
  ("(var3 stable)" 74 297)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 71)
  ("(var4 stable)" 71 297)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 67)
  ("(var1 stable)" 67 297)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 61)
  ("(var2 up)" 61 179)
  ("(var2 down)" 179 181)
  ("(var2 stable)" 181 297)
 )
)
(81
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 84)
  ("(var3 stable)" 84 312)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 80)
  ("(var4 stable)" 80 312)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 83)
  ("(var1 stable)" 83 312)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 66)
  ("(var2 down)" 66 71)
  ("(var2 up)" 71 197)
  ("(var2 stable)" 197 312)
 )
)
(82
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 87)
  ("(var3 stable)" 87 316)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 86)
  ("(var4 stable)" 86 316)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 50)
  ("(var1 stable)" 50 54)
  ("(var1 up)" 54 84)
  ("(var1 stable)" 84 316)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 72)
  ("(var2 down)" 72 77)
  ("(var2 up)" 77 202)
  ("(var2 stable)" 202 316)
 )
)
(83
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 101)
  ("(var3 stable)" 101 332)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 104)
  ("(var4 stable)" 104 332)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 76)
  ("(var1 up)" 76 102)
  ("(var1 stable)" 102 104)
  ("(var1 up)" 104 107)
  ("(var1 stable)" 107 332)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 up)" 96 223)
  ("(var2 stable)" 223 332)
 )
)
(84
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 59)
  ("(var3 stable)" 59 61)
  ("(var3 up)" 61 84)
  ("(var3 stable)" 84 303)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 92)
  ("(var4 stable)" 92 303)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 83)
  ("(var1 stable)" 83 303)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 72)
  ("(var2 down)" 72 77)
  ("(var2 up)" 77 176)
  ("(var2 stable)" 176 303)
 )
)
(85
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 91)
  ("(var3 stable)" 91 324)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 89)
  ("(var4 stable)" 89 324)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 94)
  ("(var1 stable)" 94 324)
  ("(var2 stable)" 0 74)
  ("(var2 up)" 74 76)
  ("(var2 down)" 76 81)
  ("(var2 stable)" 81 124)
  ("(var2 up)" 124 205)
  ("(var2 stable)" 205 324)
 )
)
(86
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 110)
  ("(var3 stable)" 110 349)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 108)
  ("(var4 stable)" 108 349)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 107)
  ("(var1 stable)" 107 349)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 up)" 96 237)
  ("(var2 stable)" 237 349)
 )
)
(87
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 121)
  ("(var3 stable)" 121 123)
  ("(var3 up)" 123 125)
  ("(var3 stable)" 125 365)
  ("(var4 stable)" 0 91)
  ("(var4 up)" 91 118)
  ("(var4 stable)" 118 120)
  ("(var4 up)" 120 123)
  ("(var4 down)" 123 125)
  ("(var4 up)" 125 132)
  ("(var4 stable)" 132 365)
  ("(var1 stable)" 0 87)
  ("(var1 up)" 87 121)
  ("(var1 stable)" 121 123)
  ("(var1 up)" 123 125)
  ("(var1 stable)" 125 365)
  ("(var2 stable)" 0 109)
  ("(var2 up)" 109 112)
  ("(var2 down)" 112 116)
  ("(var2 up)" 116 258)
  ("(var2 stable)" 258 365)
 )
)
(88
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 77)
  ("(var3 up)" 77 79)
  ("(var3 down)" 79 81)
  ("(var3 up)" 81 117)
  ("(var3 stable)" 117 356)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 114)
  ("(var4 stable)" 114 356)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 109)
  ("(var1 stable)" 109 354)
  ("(var1 down)" 354 356)
  ("(var2 stable)" 0 93)
  ("(var2 up)" 93 95)
  ("(var2 down)" 95 100)
  ("(var2 up)" 100 151)
  ("(var2 stable)" 151 153)
  ("(var2 up)" 153 240)
  ("(var2 down)" 240 242)
  ("(var2 stable)" 242 356)
 )
)
(89
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 68)
  ("(var3 stable)" 68 293)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 66)
  ("(var4 stable)" 66 293)
  ("(var1 stable)" 0 28)
  ("(var1 up)" 28 65)
  ("(var1 stable)" 65 293)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 52)
  ("(var2 down)" 52 57)
  ("(var2 up)" 57 147)
  ("(var2 down)" 147 149)
  ("(var2 up)" 149 190)
  ("(var2 down)" 190 192)
  ("(var2 up)" 192 194)
  ("(var2 stable)" 194 293)
 )
)
(90
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 77)
  ("(var3 stable)" 77 80)
  ("(var3 up)" 80 82)
  ("(var3 stable)" 82 333)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 75)
  ("(var4 down)" 75 77)
  ("(var4 up)" 77 86)
  ("(var4 stable)" 86 333)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 81)
  ("(var1 stable)" 81 333)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 66)
  ("(var2 down)" 66 71)
  ("(var2 stable)" 71 117)
  ("(var2 up)" 117 177)
  ("(var2 stable)" 177 179)
  ("(var2 up)" 179 210)
  ("(var2 stable)" 210 333)
 )
)
(91
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 78)
  ("(var3 stable)" 78 325)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 77)
  ("(var4 stable)" 77 325)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 78)
  ("(var1 stable)" 78 325)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 64)
  ("(var2 down)" 64 69)
  ("(var2 up)" 69 223)
  ("(var2 stable)" 223 325)
 )
)
(92
 (
  ("(var3 stable)" 0 94)
  ("(var3 up)" 94 96)
  ("(var3 stable)" 96 100)
  ("(var3 up)" 100 106)
  ("(var3 stable)" 106 108)
  ("(var3 up)" 108 125)
  ("(var3 stable)" 125 378)
  ("(var4 stable)" 0 99)
  ("(var4 up)" 99 126)
  ("(var4 stable)" 126 378)
  ("(var1 stable)" 0 98)
  ("(var1 up)" 98 129)
  ("(var1 stable)" 129 378)
  ("(var2 stable)" 0 112)
  ("(var2 up)" 112 114)
  ("(var2 down)" 114 119)
  ("(var2 up)" 119 230)
  ("(var2 stable)" 230 378)
 )
)
(93
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 98)
  ("(var3 stable)" 98 311)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 102)
  ("(var4 stable)" 102 311)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 96)
  ("(var1 stable)" 96 311)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 86)
  ("(var2 up)" 86 199)
  ("(var2 down)" 199 201)
  ("(var2 up)" 201 203)
  ("(var2 down)" 203 205)
  ("(var2 stable)" 205 311)
 )
)
(94
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 122)
  ("(var3 stable)" 122 347)
  ("(var4 stable)" 0 88)
  ("(var4 up)" 88 120)
  ("(var4 stable)" 120 347)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 119)
  ("(var1 stable)" 119 122)
  ("(var1 up)" 122 124)
  ("(var1 stable)" 124 347)
  ("(var2 stable)" 0 104)
  ("(var2 up)" 104 106)
  ("(var2 down)" 106 111)
  ("(var2 stable)" 111 150)
  ("(var2 up)" 150 152)
  ("(var2 stable)" 152 154)
  ("(var2 up)" 154 227)
  ("(var2 stable)" 227 347)
 )
)
(95
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 101)
  ("(var3 stable)" 101 333)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 98)
  ("(var4 stable)" 98 333)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 100)
  ("(var1 stable)" 100 333)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 86)
  ("(var2 down)" 86 91)
  ("(var2 up)" 91 212)
  ("(var2 down)" 212 214)
  ("(var2 up)" 214 216)
  ("(var2 stable)" 216 333)
 )
)
(96
 (
  ("(var3 stable)" 0 97)
  ("(var3 up)" 97 136)
  ("(var3 stable)" 136 387)
  ("(var4 stable)" 0 98)
  ("(var4 up)" 98 128)
  ("(var4 stable)" 128 387)
  ("(var1 stable)" 0 98)
  ("(var1 up)" 98 131)
  ("(var1 stable)" 131 387)
  ("(var2 stable)" 0 116)
  ("(var2 up)" 116 120)
  ("(var2 down)" 120 124)
  ("(var2 up)" 124 224)
  ("(var2 down)" 224 226)
  ("(var2 up)" 226 240)
  ("(var2 down)" 240 242)
  ("(var2 up)" 242 244)
  ("(var2 stable)" 244 387)
 )
)
(97
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 44)
  ("(var3 down)" 44 46)
  ("(var3 up)" 46 72)
  ("(var3 stable)" 72 316)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 74)
  ("(var4 stable)" 74 316)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 76)
  ("(var1 stable)" 76 316)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 64)
  ("(var2 up)" 64 195)
  ("(var2 stable)" 195 316)
 )
)
(98
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 74)
  ("(var3 stable)" 74 77)
  ("(var3 up)" 77 79)
  ("(var3 stable)" 79 339)
  ("(var4 stable)" 0 50)
  ("(var4 up)" 50 75)
  ("(var4 stable)" 75 339)
  ("(var1 stable)" 0 42)
  ("(var1 down)" 42 44)
  ("(var1 up)" 44 81)
  ("(var1 stable)" 81 339)
  ("(var2 stable)" 0 63)
  ("(var2 up)" 63 65)
  ("(var2 down)" 65 70)
  ("(var2 stable)" 70 117)
  ("(var2 up)" 117 190)
  ("(var2 stable)" 190 339)
 )
)
(99
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 98)
  ("(var3 stable)" 98 326)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 93)
  ("(var4 stable)" 93 326)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 107)
  ("(var1 stable)" 107 326)
  ("(var2 stable)" 0 84)
  ("(var2 down)" 84 89)
  ("(var2 up)" 89 207)
  ("(var2 stable)" 207 326)
 )
)
(100
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 44)
  ("(var3 down)" 44 46)
  ("(var3 up)" 46 76)
  ("(var3 stable)" 76 326)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 74)
  ("(var4 stable)" 74 326)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 85)
  ("(var1 stable)" 85 326)
  ("(var2 stable)" 0 60)
  ("(var2 up)" 60 62)
  ("(var2 down)" 62 67)
  ("(var2 stable)" 67 112)
  ("(var2 up)" 112 199)
  ("(var2 stable)" 199 326)
 )
)
